Nuprl Definition : unique_set
2,24
postcript
pdf
{!
x
:
T
|
P
(
x
)} == {
x
:
T
|
P
(
x
) & (
y
:
T
.
P
(
y
)
y
=
x
) }
latex
clarification:
{!
x
:
T
|
P
(
x
)} == {
x
:
T
|
P
(
x
) & (
y
:
T
.
P
(
y
)
y
=
x
T
) }
latex
Definitions
P
&
Q
,
x
:
A
.
B
(
x
)
,
P
Q
FDL editor aliases
unique_set
origin
y:T. P(y) 
y = x) }
y:T. P(y) y = x 
T) } y:T. P(y) y = x) }
y:T. P(y) y = x T) } x:A. B(x) Q